type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
var $Heap : [ref, name]any;
function IsHeap<any>(h : [ref, name]any) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $writable : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall<any> T : name, h : [ref, name]any :: (IsHeap(h) ==> h[ClassRepr(T), $writable]));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($writable);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom (forall<any> T : name, h : [ref, name]any :: {h[ClassRepr(T), $writable]} (IsHeap(h) ==> h[ClassRepr(T), $writable]));
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($writable);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall<any> a : ref, T : name, i : int, r : int, heap : [ref, name]any :: (($typeof(a) <: RefArray(T, r)) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {$Is(a, ValueArray(T, r))} ($Is(a, ValueArray(T, r)) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {$Is(a, RefArray(T, r))} ($Is(a, RefArray(T, r)) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const System.Array : name;
axiom $IsClass(System.Array);
axiom (System.Array <: System.Object);
axiom (forall T : name :: ((System.Array <: T) ==> ((T == System.Array) || (System.Object <: T))));
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~ak : name);
function $StructGet<any>($$unnamed~am : struct, $$unnamed~al : name) returns ($$unnamed~an : any);
function $StructSet<any>($$unnamed~aq : struct, $$unnamed~ap : name, $$unnamed~ao : any) returns ($$unnamed~ar : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~as : bool);
function $typeof($$unnamed~at : ref) returns ($$unnamed~au : name);
function Implements(class : name, interface : name) returns ($$unnamed~av : bool);
axiom (forall T : name, J : name :: {Implements(T, J)} (Implements(T, J) ==> (T <: J)));
function InterfaceExtends(subIntf : name, superIntf : name) returns ($$unnamed~aw : bool);
axiom (forall J : name, K : name :: {InterfaceExtends(J, K)} (InterfaceExtends(J, K) ==> (J <: K)));
function $IsClass($$unnamed~ax : name) returns ($$unnamed~ay : bool);
function DirectBase(class : name) returns (directBaseClass : name);
axiom (forall C : name :: (C <: DirectBase(C)));
axiom (forall T : name, U : name :: ((($IsClass(T) && $IsClass(U)) && (T <: U)) ==> ((T == U) || ((T != System.Object) && (DirectBase(T) <: U)))));
function $IsInterface($$unnamed~az : name) returns ($$unnamed~ba : bool);
axiom (forall J : name :: {$IsInterface(J)} ($IsInterface(J) ==> (J <: System.Object)));
function $IsValueType($$unnamed~bb : name) returns ($$unnamed~bc : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
axiom (forall T : name, U : name, o : ref :: ((((((o != null) && $IsClass(T)) && $IsClass(U)) && !(T <: U)) && !(U <: T)) ==> !($Is(o, T) && $Is(o, U))));
const System.Object : name;
axiom $IsClass(System.Object);
function $IsTokenForType($$unnamed~be : struct, $$unnamed~bd : name) returns ($$unnamed~bf : bool);
function TypeObject($$unnamed~bg : name) returns ($$unnamed~bh : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function $Is($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bp : ref, $$unnamed~bo : name) returns ($$unnamed~bq : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall<any> heap : [ref, name]any, o : ref, A : name, r : int :: ($Is(o, RefArray(A, r)) ==> (heap[o, $inv] == $typeof(o))));
axiom (forall<any> heap : [ref, name]any, o : ref, A : name, r : int :: (((IsHeap(heap) && (o != null)) && $Is(o, ValueArray(A, r))) ==> (heap[o, $inv] == $typeof(o))));
function IsAllocated<any>(h : [ref, name]any, o : any) returns ($$unnamed~br : bool);
axiom (forall<any> h : [ref, name]any, o : ref, f : name :: {IsAllocated(h, h[o, f])} (IsHeap(h) ==> IsAllocated(h, h[o, f])));
axiom (forall<any> h : [ref, name]any, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall<any> h : [ref, name]any, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall<any> h : [ref, name]any, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall<any> h : [ref, name]any, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall<any> h : [ref, name]any, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall<any> h : [ref, name]any, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (IsHeap(h) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall<any> h : [ref, name]any, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function AsOwnedField(f : name) returns ($$unnamed~bs : name);
axiom (forall<any> h : [ref, name]any, o : ref, f : name :: {h[o, AsOwnedField(f)]} ((IsHeap(h) && (h[o, $inv] <: DeclType(AsOwnedField(f)))) ==> ((h[o, AsOwnedField(f)] == null) || !h[h[o, AsOwnedField(f)], $writable])));
axiom (forall<any> h : [ref, name]any, o : ref :: {h[o, $writable]} ((IsHeap(h) && !h[o, $writable]) ==> (h[o, $inv] == $typeof(o))));
function Box<any>($$unnamed~bu : any, $$unnamed~bt : ref) returns ($$unnamed~bv : ref);
function Unbox<any>($$unnamed~bw : ref) returns ($$unnamed~bx : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
axiom (forall<any> heap : [ref, name]any, x : any, p : ref :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> (heap[Box(x, p), $inv] == $typeof(Box(x, p)))));
function UnboxedType($$unnamed~by : ref) returns ($$unnamed~bz : name);
function BoxTester(p : ref, typ : name) returns ($$unnamed~ca : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.Int16.MinValue : int;
const System.Int16.MaxValue : int;
const System.Int32.MinValue : int;
const System.Int32.MaxValue : int;
const System.Int64.MinValue : int;
const System.Int64.MaxValue : int;
axiom (System.Int64.MinValue < System.Int32.MinValue);
axiom (System.Int32.MinValue < System.Int16.MinValue);
axiom (System.Int16.MinValue < System.Int16.MaxValue);
axiom (System.Int16.MaxValue < System.Int32.MaxValue);
axiom (System.Int32.MaxValue < System.Int64.MaxValue);
function InRange(i : int, T : name) returns ($$unnamed~cb : bool);
axiom (forall i : int :: (InRange(i, System.Int16) <==> ((System.Int16.MinValue <= i) && (i <= System.Int16.MaxValue))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((System.Int32.MinValue <= i) && (i <= System.Int32.MaxValue))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((System.Int64.MinValue <= i) && (i <= System.Int64.MaxValue))));
function $RealFromInt($$unnamed~cd : real, $$unnamed~cc : int) returns ($$unnamed~ce : bool);
function $IntFromReal($$unnamed~cg : int, $$unnamed~cf : real) returns ($$unnamed~ch : bool);
function $SizeIs($$unnamed~cj : name, $$unnamed~ci : int) returns ($$unnamed~ck : bool);
function $IfThenElse<any>($$unnamed~cn : bool, $$unnamed~cm : any, $$unnamed~cl : any) returns ($$unnamed~co : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cp : int) returns ($$unnamed~cq : int);
function #rneg($$unnamed~cr : real) returns ($$unnamed~cs : real);
function #rdiv($$unnamed~cu : real, $$unnamed~ct : real) returns ($$unnamed~cv : real);
function #and($$unnamed~cx : int, $$unnamed~cw : int) returns ($$unnamed~cy : int);
function #or($$unnamed~da : int, $$unnamed~cz : int) returns ($$unnamed~db : int);
function #xor($$unnamed~dd : int, $$unnamed~dc : int) returns ($$unnamed~de : int);
function #shl($$unnamed~dg : int, $$unnamed~df : int) returns ($$unnamed~dh : int);
function #shr($$unnamed~dj : int, $$unnamed~di : int) returns ($$unnamed~dk : int);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
const $UnknownRef : ref;
const RTE.CallStack : name;
const RTE.Instructions : name;
const RTE.Data : name;
const RTE.MStackBase : name;
const RTE.CurrRTEMode : name;
const RTE.C : name;
const RTE.A : name;
const RTE.MSP : name;
const RTE.MStackMaxSize : name;
const RTE.CSP : name;
const RTE.Scratch : name;
const RTE.Program : name;
const RTE.Z : name;
const RTE.RtnCode : name;
const RTE.DPP : name;
const RTE.PC : name;
const Memory.contents : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const RTE : name;
const System.Boolean : name;
const System.Exception : name;
const Memory : name;
const System.Runtime.Serialization.ISerializable : name;
const System.Byte : name;
const Microsoft.Contracts.GuardException : name;
const Microsoft.Contracts.ICheckedException : name;
const System.Runtime.InteropServices._Exception : name;
axiom !IsStaticField(Memory.contents);
axiom IsDirectlyModifiableField(Memory.contents);
axiom (AsOwnedField(Memory.contents) == Memory.contents);
axiom (DeclType(Memory.contents) == Memory);
axiom (AsNonNullRefField(Memory.contents, ValueArray(System.Byte, 1)) == Memory.contents);
function #System.Array.get_Length($$unnamed~dl : ref) returns ($$unnamed~dm : int);
function #Memory.get_cont$System.Int32<any>($$unnamed~dp : [ref, name]any, $$unnamed~do : ref, $$unnamed~dn : int) returns ($$unnamed~dq : int);
axiom !IsStaticField(RTE.CallStack);
axiom IsDirectlyModifiableField(RTE.CallStack);
axiom (AsOwnedField(RTE.CallStack) == RTE.CallStack);
axiom (DeclType(RTE.CallStack) == RTE);
axiom (AsNonNullRefField(RTE.CallStack, ValueArray(System.Int32, 1)) == RTE.CallStack);
axiom !IsStaticField(RTE.CSP);
axiom IsDirectlyModifiableField(RTE.CSP);
axiom (AsOwnedField(RTE.CSP) == RTE.CSP);
axiom (DeclType(RTE.CSP) == RTE);
axiom (AsRangeField(RTE.CSP, System.Int32) == RTE.CSP);
axiom !IsStaticField(RTE.MStackBase);
axiom IsDirectlyModifiableField(RTE.MStackBase);
axiom (AsOwnedField(RTE.MStackBase) == RTE.MStackBase);
axiom (DeclType(RTE.MStackBase) == RTE);
axiom (AsRangeField(RTE.MStackBase, System.Int32) == RTE.MStackBase);
axiom !IsStaticField(RTE.MSP);
axiom IsDirectlyModifiableField(RTE.MSP);
axiom (AsOwnedField(RTE.MSP) == RTE.MSP);
axiom (DeclType(RTE.MSP) == RTE);
axiom (AsRangeField(RTE.MSP, System.Int32) == RTE.MSP);
axiom !IsStaticField(RTE.MStackMaxSize);
axiom IsDirectlyModifiableField(RTE.MStackMaxSize);
axiom (AsOwnedField(RTE.MStackMaxSize) == RTE.MStackMaxSize);
axiom (DeclType(RTE.MStackMaxSize) == RTE);
axiom (AsRangeField(RTE.MStackMaxSize, System.Int32) == RTE.MStackMaxSize);
axiom !IsStaticField(RTE.DPP);
axiom IsDirectlyModifiableField(RTE.DPP);
axiom (AsOwnedField(RTE.DPP) == RTE.DPP);
axiom (DeclType(RTE.DPP) == RTE);
axiom (AsRangeField(RTE.DPP, System.Int32) == RTE.DPP);
axiom !IsStaticField(RTE.A);
axiom IsDirectlyModifiableField(RTE.A);
axiom (AsOwnedField(RTE.A) == RTE.A);
axiom (DeclType(RTE.A) == RTE);
axiom (AsRangeField(RTE.A, System.Int32) == RTE.A);
axiom !IsStaticField(RTE.Z);
axiom IsDirectlyModifiableField(RTE.Z);
axiom (AsOwnedField(RTE.Z) == RTE.Z);
axiom (DeclType(RTE.Z) == RTE);
axiom !IsStaticField(RTE.C);
axiom IsDirectlyModifiableField(RTE.C);
axiom (AsOwnedField(RTE.C) == RTE.C);
axiom (DeclType(RTE.C) == RTE);
axiom !IsStaticField(RTE.PC);
axiom IsDirectlyModifiableField(RTE.PC);
axiom (AsOwnedField(RTE.PC) == RTE.PC);
axiom (DeclType(RTE.PC) == RTE);
axiom (AsRangeField(RTE.PC, System.Int32) == RTE.PC);
axiom !IsStaticField(RTE.CurrRTEMode);
axiom IsDirectlyModifiableField(RTE.CurrRTEMode);
axiom (AsOwnedField(RTE.CurrRTEMode) == RTE.CurrRTEMode);
axiom (DeclType(RTE.CurrRTEMode) == RTE);
axiom (AsRangeField(RTE.CurrRTEMode, System.Int32) == RTE.CurrRTEMode);
axiom !IsStaticField(RTE.RtnCode);
axiom IsDirectlyModifiableField(RTE.RtnCode);
axiom (AsOwnedField(RTE.RtnCode) == RTE.RtnCode);
axiom (DeclType(RTE.RtnCode) == RTE);
axiom (AsRangeField(RTE.RtnCode, System.Int32) == RTE.RtnCode);
axiom !IsStaticField(RTE.Program);
axiom IsDirectlyModifiableField(RTE.Program);
axiom (AsOwnedField(RTE.Program) == RTE.Program);
axiom (DeclType(RTE.Program) == RTE);
axiom (AsNonNullRefField(RTE.Program, Memory) == RTE.Program);
axiom !IsStaticField(RTE.Data);
axiom IsDirectlyModifiableField(RTE.Data);
axiom (AsOwnedField(RTE.Data) == RTE.Data);
axiom (DeclType(RTE.Data) == RTE);
axiom (AsNonNullRefField(RTE.Data, Memory) == RTE.Data);
axiom !IsStaticField(RTE.Scratch);
axiom IsDirectlyModifiableField(RTE.Scratch);
axiom (AsOwnedField(RTE.Scratch) == RTE.Scratch);
axiom (DeclType(RTE.Scratch) == RTE);
axiom (AsNonNullRefField(RTE.Scratch, Memory) == RTE.Scratch);
axiom !IsStaticField(RTE.Instructions);
axiom IsDirectlyModifiableField(RTE.Instructions);
axiom (AsOwnedField(RTE.Instructions) == RTE.Instructions);
axiom (DeclType(RTE.Instructions) == RTE);
axiom (AsNonNullRefField(RTE.Instructions, ValueArray(System.Int32, 1)) == RTE.Instructions);
function #System.Array.get_Rank($$unnamed~dr : ref) returns ($$unnamed~ds : int);
function #System.Array.GetLowerBound$System.Int32($$unnamed~du : ref, $$unnamed~dt : int) returns ($$unnamed~dv : int);
function #RTE.apply$System.Int32$System.Int32$System.Int32($$unnamed~dy : int, $$unnamed~dx : int, $$unnamed~dw : int) returns ($$unnamed~dz : int);
function #RTE.carry$System.Int32$System.Int32$System.Int32($$unnamed~ec : int, $$unnamed~eb : int, $$unnamed~ea : int) returns ($$unnamed~ed : bool);
function #RTE.DP<any>($$unnamed~ef : [ref, name]any, $$unnamed~ee : ref) returns ($$unnamed~eg : int);
axiom $IsClass(Memory);
axiom (DirectBase(Memory) == System.Object);
axiom (forall K : name :: {(Memory <: K)} ((Memory <: K) <==> ((Memory == K) || (System.Object <: K))));
axiom (forall U : name :: {(U <: Memory)} ((U <: Memory) ==> (U == Memory)));
function Inv_Memory<any>(object : ref, heap : [ref, name]any) returns (result : bool);
axiom (forall<any> this : ref, heap : [ref, name]any :: {Inv_Memory(this, heap)} (Inv_Memory(this, heap) <==> true));
axiom (forall<any> o : ref, heap : [ref, name]any :: {(heap[o, $inv] <: Memory)} {Inv_Memory(o, heap)} ((IsHeap(heap) && (heap[o, $inv] <: Memory)) ==> Inv_Memory(o, heap)));
procedure Memory..ctor$System.Int32(this : ref, n$in : int);
  requires (0 < n$in);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || (old($Heap)[$o, $inv] == $Heap[$o, $inv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  

procedure System.Object..ctor(this : ref);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || (old($Heap)[$o, $inv] == $Heap[$o, $inv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == System.Object));
  

procedure Memory.get_cont$System.Int32(this : ref, addr$in : int) returns ($result : int);
  requires (0 <= addr$in);
  requires (addr$in < $Length($Heap[this, Memory.contents]));
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures ($Heap == old($Heap));
  free ensures ($result == #Memory.get_cont$System.Int32($Heap, this, addr$in));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  

procedure Memory.set_cont$System.Int32$System.Byte(this : ref, addr$in : int, value$in : int);
  requires (0 <= addr$in);
  requires (addr$in < $Length($Heap[this, Memory.contents]));
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  

procedure Memory.inSandbox$System.Int32(this : ref, addr$in : int) returns ($result : bool);
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  ensures (!$result || ((0 <= addr$in) && (addr$in < $Length($Heap[this, Memory.contents]))));
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Memory));
  

axiom $IsClass(RTE);
axiom (DirectBase(RTE) == System.Object);
axiom (forall K : name :: {(RTE <: K)} ((RTE <: K) <==> ((RTE == K) || (System.Object <: K))));
function Inv_RTE<any>(object : ref, heap : [ref, name]any) returns (result : bool);
axiom (forall<any> this : ref, heap : [ref, name]any :: {Inv_RTE(this, heap)} (Inv_RTE(this, heap) <==> ((((((((((($Length(heap[this, RTE.CallStack]) == 10) && (0 <= heap[this, RTE.CSP])) && (heap[this, RTE.CSP] <= 10)) && (heap[this, RTE.MStackBase] <= heap[this, RTE.MSP])) && (heap[this, RTE.MSP] <= (heap[this, RTE.MStackBase] + heap[this, RTE.MStackMaxSize]))) && ((heap[this, RTE.MSP] % 4) == 0)) && ((heap[this, RTE.MStackBase] % 4) == 0)) && ((heap[this, RTE.MStackMaxSize] % 4) == 0)) && (0 <= heap[this, RTE.MStackBase])) && (0 <= heap[this, RTE.MStackMaxSize])) && (0 <= heap[this, RTE.DPP]))));
axiom (forall<any> o : ref, heap : [ref, name]any :: {(heap[o, $inv] <: RTE)} {Inv_RTE(o, heap)} ((IsHeap(heap) && (heap[o, $inv] <: RTE)) ==> Inv_RTE(o, heap)));
procedure RTE.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool);
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  

axiom $IsClass(Microsoft.Contracts.ObjectInvariantException);
axiom $IsClass(Microsoft.Contracts.GuardException);
axiom $IsClass(System.Exception);
axiom (DirectBase(System.Exception) == System.Object);
axiom $IsInterface(System.Runtime.Serialization.ISerializable);
axiom (forall K : name :: {(System.Runtime.Serialization.ISerializable <: K)} ((System.Runtime.Serialization.ISerializable <: K) <==> ((System.Runtime.Serialization.ISerializable == K) || (System.Object == K))));
axiom Implements(System.Exception, System.Runtime.Serialization.ISerializable);
axiom $IsInterface(System.Runtime.InteropServices._Exception);
axiom (forall K : name :: {(System.Runtime.InteropServices._Exception <: K)} ((System.Runtime.InteropServices._Exception <: K) <==> ((System.Runtime.InteropServices._Exception == K) || (System.Object == K))));
axiom Implements(System.Exception, System.Runtime.InteropServices._Exception);
axiom (forall K : name :: {(System.Exception <: K)} ((System.Exception <: K) <==> ((((System.Exception == K) || (System.Object <: K)) || (System.Runtime.Serialization.ISerializable <: K)) || (System.Runtime.InteropServices._Exception <: K))));
function Inv_System.Exception<any>(object : ref, heap : [ref, name]any) returns (result : bool);
axiom (forall<any> this : ref, heap : [ref, name]any :: {Inv_System.Exception(this, heap)} (Inv_System.Exception(this, heap) <==> true));
axiom (forall<any> o : ref, heap : [ref, name]any :: {(heap[o, $inv] <: System.Exception)} {Inv_System.Exception(o, heap)} ((IsHeap(heap) && (heap[o, $inv] <: System.Exception)) ==> Inv_System.Exception(o, heap)));
axiom (DirectBase(Microsoft.Contracts.GuardException) == System.Exception);
axiom (forall K : name :: {(Microsoft.Contracts.GuardException <: K)} ((Microsoft.Contracts.GuardException <: K) <==> ((Microsoft.Contracts.GuardException == K) || (System.Exception <: K))));
function Inv_Microsoft.Contracts.GuardException<any>(object : ref, heap : [ref, name]any) returns (result : bool);
axiom (forall<any> this : ref, heap : [ref, name]any :: {Inv_Microsoft.Contracts.GuardException(this, heap)} (Inv_Microsoft.Contracts.GuardException(this, heap) <==> true));
axiom (forall<any> o : ref, heap : [ref, name]any :: {(heap[o, $inv] <: Microsoft.Contracts.GuardException)} {Inv_Microsoft.Contracts.GuardException(o, heap)} ((IsHeap(heap) && (heap[o, $inv] <: Microsoft.Contracts.GuardException)) ==> Inv_Microsoft.Contracts.GuardException(o, heap)));
axiom (DirectBase(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom (forall K : name :: {(Microsoft.Contracts.ObjectInvariantException <: K)} ((Microsoft.Contracts.ObjectInvariantException <: K) <==> ((Microsoft.Contracts.ObjectInvariantException == K) || (Microsoft.Contracts.GuardException <: K))));
function Inv_Microsoft.Contracts.ObjectInvariantException<any>(object : ref, heap : [ref, name]any) returns (result : bool);
axiom (forall<any> this : ref, heap : [ref, name]any :: {Inv_Microsoft.Contracts.ObjectInvariantException(this, heap)} (Inv_Microsoft.Contracts.ObjectInvariantException(this, heap) <==> true));
axiom (forall<any> o : ref, heap : [ref, name]any :: {(heap[o, $inv] <: Microsoft.Contracts.ObjectInvariantException)} {Inv_Microsoft.Contracts.ObjectInvariantException(o, heap)} ((IsHeap(heap) && (heap[o, $inv] <: Microsoft.Contracts.ObjectInvariantException)) ==> Inv_Microsoft.Contracts.ObjectInvariantException(o, heap)));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || (old($Heap)[$o, $inv] == $Heap[$o, $inv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException));
  

procedure RTE..ctor$System.Int32.array$notnull$System.Int32$System.Int32(this : ref, input$in : ref, baseAddress$in : int, size$in : int);
  requires (0 <= baseAddress$in);
  requires ((baseAddress$in % 4) == 0);
  requires (0 <= size$in);
  requires ((size$in % 4) == 0);
  requires ((baseAddress$in + size$in) <= 254);
  requires (($Heap[input$in, $writable] == true) && ($Heap[input$in, $inv] == $typeof(input$in)));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || (old($Heap)[$o, $inv] == $Heap[$o, $inv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  ensures (($Heap[input$in, $writable] == true) && ($Heap[input$in, $inv] == $typeof(input$in)));
  

procedure System.Array.Copy$System.Array$notnull$System.Int32$System.Array$notnull$System.Int32$System.Int32(sourceArray$in : ref, sourceIndex$in : int, destinationArray$in : ref, destinationIndex$in : int, length$in : int);
  requires (sourceArray$in != null);
  requires (destinationArray$in != null);
  requires ($Rank(sourceArray$in) == $Rank(destinationArray$in));
  requires (sourceIndex$in >= $LBound(sourceArray$in, 0));
  requires (destinationIndex$in >= $LBound(destinationArray$in, 0));
  requires (length$in >= 0);
  requires ((sourceIndex$in + length$in) <= ($LBound(sourceArray$in, 0) + $Length(sourceArray$in)));
  requires ((destinationIndex$in + length$in) <= ($LBound(destinationArray$in, 0) + $Length(destinationArray$in)));
  requires (($Heap[sourceArray$in, $writable] == true) && ($Heap[sourceArray$in, $inv] == $typeof(sourceArray$in)));
  requires (($Heap[destinationArray$in, $writable] == true) && ($Heap[destinationArray$in, $inv] == $typeof(destinationArray$in)));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[sourceArray$in, $writable] == true) && ($Heap[sourceArray$in, $inv] == $typeof(sourceArray$in)));
  ensures (($Heap[destinationArray$in, $writable] == true) && ($Heap[destinationArray$in, $inv] == $typeof(destinationArray$in)));
  

procedure RTE.apply$System.Int32$System.Int32$System.Int32(op$in : int, a$in : int, b$in : int) returns ($result : int);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures ($Heap == old($Heap));
  free ensures ($result == #RTE.apply$System.Int32$System.Int32$System.Int32(op$in, a$in, b$in));
  

procedure RTE.ApplyQuad$System.Int32$System.Int32$System.Int32(this : ref, op$in : int, a$in : int, b$in : int) returns ($result : int);
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  

procedure RTE.carry$System.Int32$System.Int32$System.Int32(op$in : int, a$in : int, b$in : int) returns ($result : bool);
  requires ((op$in == 30) || (op$in == 31));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures ($Heap == old($Heap));
  free ensures ($result == #RTE.carry$System.Int32$System.Int32$System.Int32(op$in, a$in, b$in));
  

procedure RTE.ReadQuad$Memory$notnull$System.Int32(m$in : ref, addr$in : int) returns ($result : int);
  requires (0 <= addr$in);
  requires (addr$in <= ($Length($Heap[m$in, Memory.contents]) - 4));
  requires (($Heap[m$in, $writable] == true) && ($Heap[m$in, $inv] == $typeof(m$in)));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[m$in, $writable] == true) && ($Heap[m$in, $inv] == $typeof(m$in)));
  

procedure RTE.WriteQuad$Memory$notnull$System.Int32$System.Int32(m$in : ref, addr$in : int, value$in : int);
  requires (0 <= addr$in);
  requires (addr$in <= ($Length($Heap[m$in, Memory.contents]) - 4));
  requires (($Heap[m$in, $writable] == true) && ($Heap[m$in, $inv] == $typeof(m$in)));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[m$in, $writable] == true) && ($Heap[m$in, $inv] == $typeof(m$in)));
  

procedure RTE.DP(this : ref) returns ($result : int);
  requires (((((((((((((($Heap[this, $writable] == true) && ($Heap[this, $inv] == System.Object)) && ($Heap[$Heap[this, RTE.Instructions], $writable] == true)) && ($Heap[$Heap[this, RTE.Instructions], $inv] == $typeof($Heap[this, RTE.Instructions]))) && ($Heap[$Heap[this, RTE.Program], $writable] == true)) && ($Heap[$Heap[this, RTE.Program], $inv] == $typeof($Heap[this, RTE.Program]))) && ($Heap[$Heap[this, RTE.Data], $writable] == true)) && ($Heap[$Heap[this, RTE.Data], $inv] == $typeof($Heap[this, RTE.Data]))) && ($Heap[$Heap[this, RTE.Scratch], $writable] == true)) && ($Heap[$Heap[this, RTE.Scratch], $inv] == $typeof($Heap[this, RTE.Scratch]))) && ($Heap[$Heap[this, RTE.CallStack], $writable] == true)) && ($Heap[$Heap[this, RTE.CallStack], $inv] == $typeof($Heap[this, RTE.CallStack]))) && Inv_RTE(this, $Heap)) && (($Heap[this, RTE.DPP] + 1) < $Length($Heap[$Heap[this, RTE.Scratch], Memory.contents])));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures ($Heap == old($Heap));
  free ensures ($result == #RTE.DP($Heap, this));
  

procedure RTE.Terminate$System.Int32(this : ref, code$in : int);
  requires (($Heap[this, $writable] == true) && (System.Object <: $Heap[this, $inv]));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  

procedure RTE.Run(this : ref) returns ($result : int);
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  

procedure RTE.ExecuteInstruction(this : ref);
  requires (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  ensures (($Heap[this, $writable] == true) && ($Heap[this, $inv] == RTE));
  

procedure RTE.ApplyALU$System.Int32$System.Int32$System.Int32(this : ref, opcd$in : int, valType$in : int, val$in : int);
  requires (((($Heap[this, $writable] == true) && (System.Object <: $Heap[this, $inv])) && ($Heap[$Heap[this, RTE.Data], $writable] == true)) && ($Heap[$Heap[this, RTE.Data], $inv] == $typeof($Heap[this, RTE.Data])));
  requires ((valType$in == 120) || (valType$in == 121));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  

implementation RTE.ExecuteInstruction(this : ref) {
  var temp0 : ref;
  var local4 : ref;
  var stack0o : ref;
  var stack1i : int;
  var currInstr : int;
  var opcd : int;
  var oprnd : int;
  var oprndType : int;
  var local10 : int;
  var stack0i : int;
  var stack0b : bool;
  var stack2i : int;
  var stack3o : ref;
  var stack4i : int;
  var stack5i : int;
  var stack3i : int;
  entry: assume IsHeap($Heap); goto $$entry~b;
  $$entry~b: assume $IsNotNull(this, RTE); goto $$entry~a;
  $$entry~a: assume ($Heap[this, $allocated] == true); goto block48637;
  block48637: temp0 := this; goto $$block48637~n;
  $$block48637~n: assert (temp0 != null); goto $$block48637~m;
  $$block48637~m: assert (($Heap[temp0, $writable] == true) && ($Heap[temp0, $inv] == RTE)); goto $$block48637~l;
  $$block48637~l: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block48637~k;
  $$block48637~k: $Heap := $Heap[$Heap[temp0, RTE.Instructions], $writable := true]; goto $$block48637~j;
  $$block48637~j: assume (($Heap[$Heap[temp0, RTE.Instructions], $writable] == true) && ($Heap[$Heap[temp0, RTE.Instructions], $inv] == $typeof($Heap[temp0, RTE.Instructions]))); goto $$block48637~i;
  $$block48637~i: $Heap := $Heap[$Heap[temp0, RTE.Program], $writable := true]; goto $$block48637~h;
  $$block48637~h: assume (($Heap[$Heap[temp0, RTE.Program], $writable] == true) && ($Heap[$Heap[temp0, RTE.Program], $inv] == $typeof($Heap[temp0, RTE.Program]))); goto $$block48637~g;
  $$block48637~g: $Heap := $Heap[$Heap[temp0, RTE.Data], $writable := true]; goto $$block48637~f;
  $$block48637~f: assume (($Heap[$Heap[temp0, RTE.Data], $writable] == true) && ($Heap[$Heap[temp0, RTE.Data], $inv] == $typeof($Heap[temp0, RTE.Data]))); goto $$block48637~e;
  $$block48637~e: $Heap := $Heap[$Heap[temp0, RTE.Scratch], $writable := true]; goto $$block48637~d;
  $$block48637~d: assume (($Heap[$Heap[temp0, RTE.Scratch], $writable] == true) && ($Heap[$Heap[temp0, RTE.Scratch], $inv] == $typeof($Heap[temp0, RTE.Scratch]))); goto $$block48637~c;
  $$block48637~c: $Heap := $Heap[$Heap[temp0, RTE.CallStack], $writable := true]; goto $$block48637~b;
  $$block48637~b: assume (($Heap[$Heap[temp0, RTE.CallStack], $writable] == true) && ($Heap[$Heap[temp0, RTE.CallStack], $inv] == $typeof($Heap[temp0, RTE.CallStack]))); goto $$block48637~a;
  $$block48637~a: local4 := null; goto block48654;
  block48654: assert (this != null); goto $$block48654~m;
  $$block48654~m: stack0o := $Heap[this, RTE.Instructions]; goto $$block48654~l;
  $$block48654~l: assume $IsNotNull(stack0o, ValueArray(System.Int32, 1)); goto $$block48654~k;
  $$block48654~k: assert (this != null); goto $$block48654~j;
  $$block48654~j: stack1i := $Heap[this, RTE.PC]; goto $$block48654~i;
  $$block48654~i: assume InRange(stack1i, System.Int32); goto $$block48654~h;
  $$block48654~h: assert (stack0o != null); goto $$block48654~g;
  $$block48654~g: assert (0 <= stack1i); goto $$block48654~f;
  $$block48654~f: assert (stack1i < $Length(stack0o)); goto $$block48654~e;
  $$block48654~e: currInstr := ValueArrayGet($Heap[stack0o, $elements], stack1i); goto $$block48654~d;
  $$block48654~d: opcd := currInstr; goto $$block48654~c;
  $$block48654~c: oprnd := 0; goto $$block48654~b;
  $$block48654~b: oprndType := 0; goto $$block48654~a;
  $$block48654~a: assume (currInstr == 85); goto block48671;
  block48671: goto block48688, block48705;
  block48688: goto block48705;
  block48705: goto block48739;
  block48739: local10 := currInstr; goto $$block48739~b;
  $$block48739~b: stack0i := 85; goto $$block48739~a;
  $$block48739~a: stack0b := (local10 == stack0i); goto true48739to48773, false48739to48756;
  true48739to48773: assume (stack0b == true); goto block48773;
  false48739to48756: assume (stack0b == false); goto block48756;
  block48773: assert (this != null); goto $$block48773~f;
  $$block48773~f: stack0i := $Heap[this, RTE.MSP]; goto $$block48773~e;
  $$block48773~e: assume InRange(stack0i, System.Int32); goto $$block48773~d;
  $$block48773~d: assert (this != null); goto $$block48773~c;
  $$block48773~c: stack1i := $Heap[this, RTE.MStackBase]; goto $$block48773~b;
  $$block48773~b: assume InRange(stack1i, System.Int32); goto $$block48773~a;
  $$block48773~a: stack0b := (stack0i == stack1i); goto true48773to49113, false48773to48790;
  block48756: goto block49147;
  true48773to49113: assume (stack0b == true); goto block49113;
  false48773to48790: assume (stack0b == false); goto block48790;
  block49113: stack0i := 23; goto $$block49113~b;
  $$block49113~b: assert (this != null); goto $$block49113~a;
  $$block49113~a: call RTE.Terminate$System.Int32(this, stack0i); goto block49130;
  block48790: assume ((((($Heap[this, RTE.MStackBase] % 4) == 0) && (($Heap[this, RTE.MSP] % 4) == 0)) && ($Heap[this, RTE.MStackBase] < $Heap[this, RTE.MSP])) ==> (($Heap[this, RTE.MStackBase] + 4) <= $Heap[this, RTE.MSP])); goto block48807;
  block49147: goto block49232;
  block49232: stack0o := null; goto $$block49232~a;
  $$block49232~a: stack0b := (local4 == stack0o); goto true49232to49300, false49232to49249;
  true49232to49300: assume (stack0b == true); goto block49300;
  false49232to49249: assume (stack0b == false); goto block49249;
  block49300: assert (temp0 != null); goto $$block49300~n;
  $$block49300~n: assert (($Heap[temp0, $writable] == true) && (System.Object <: $Heap[temp0, $inv])); goto $$block49300~m;
  $$block49300~m: assert (($Heap[temp0, $writable] == true) && ($Heap[temp0, $inv] == System.Object)); goto $$block49300~l;
  $$block49300~l: assert (($Heap[$Heap[temp0, RTE.Instructions], $writable] == true) && ($Heap[$Heap[temp0, RTE.Instructions], $inv] == $typeof($Heap[temp0, RTE.Instructions]))); goto $$block49300~k;
  $$block49300~k: assert (($Heap[$Heap[temp0, RTE.Program], $writable] == true) && ($Heap[$Heap[temp0, RTE.Program], $inv] == $typeof($Heap[temp0, RTE.Program]))); goto $$block49300~j;
  $$block49300~j: assert (($Heap[$Heap[temp0, RTE.Data], $writable] == true) && ($Heap[$Heap[temp0, RTE.Data], $inv] == $typeof($Heap[temp0, RTE.Data]))); goto $$block49300~i;
  $$block49300~i: assert (($Heap[$Heap[temp0, RTE.Scratch], $writable] == true) && ($Heap[$Heap[temp0, RTE.Scratch], $inv] == $typeof($Heap[temp0, RTE.Scratch]))); goto $$block49300~h;
  $$block49300~h: assert (($Heap[$Heap[temp0, RTE.CallStack], $writable] == true) && ($Heap[$Heap[temp0, RTE.CallStack], $inv] == $typeof($Heap[temp0, RTE.CallStack]))); goto $$block49300~g;
  $$block49300~g: assert Inv_RTE(temp0, $Heap); goto $$block49300~f;
  $$block49300~f: $Heap := $Heap[$Heap[temp0, RTE.Instructions], $writable := false]; goto $$block49300~e;
  $$block49300~e: $Heap := $Heap[$Heap[temp0, RTE.Program], $writable := false]; goto $$block49300~d;
  $$block49300~d: $Heap := $Heap[$Heap[temp0, RTE.Data], $writable := false]; goto $$block49300~c;
  $$block49300~c: $Heap := $Heap[$Heap[temp0, RTE.Scratch], $writable := false]; goto $$block49300~b;
  $$block49300~b: $Heap := $Heap[$Heap[temp0, RTE.CallStack], $writable := false]; goto $$block49300~a;
  $$block49300~a: $Heap := $Heap[temp0, $inv := RTE]; goto block49283;
  block49249: stack0o := $As(local4, Microsoft.Contracts.ICheckedException); goto true49249to49300, false49249to49266;
  block48807: goto block48824, block48926;
  block49130: goto block49147;
  true49249to49300: assume (stack0o != null); goto block49300;
  false49249to49266: assume (stack0o == null); goto block49266;
  block49266: goto block49283;
  block48824: goto block48841, block48926;
  block48926: goto block48943;
  block49283: goto block49198;
  block48841: goto block48858, block48926;
  block48943: goto block48960, block48977;
  block49198: return;
  block48858: goto block48875, block48892;
  block48960: goto block48977;
  block48977: goto block49011;
  block48875: goto block48909;
  block48892: goto block48909;
  block49011: assume ($Heap[this, RTE.MSP] <= $Length($Heap[$Heap[this, RTE.Scratch], Memory.contents])); goto block49028;
  block48909: goto block48943;
  block49028: goto block49045, block49062;
  block49045: goto block49062;
  block49062: goto block49096;
  block49096: assert (this != null); goto $$block49096~t;
  $$block49096~t: stack0o := $Heap[this, RTE.Scratch]; goto $$block49096~s;
  $$block49096~s: assume $IsNotNull(stack0o, Memory); goto $$block49096~r;
  $$block49096~r: assert (this != null); goto $$block49096~q;
  $$block49096~q: stack1i := $Heap[this, RTE.MSP]; goto $$block49096~p;
  $$block49096~p: assume InRange(stack1i, System.Int32); goto $$block49096~o;
  $$block49096~o: stack2i := 4; goto $$block49096~n;
  $$block49096~n: stack1i := (stack1i - stack2i); goto $$block49096~m;
  $$block49096~m: stack2i := -1; goto $$block49096~l;
  $$block49096~l: assert (this != null); goto $$block49096~k;
  $$block49096~k: stack3o := $Heap[this, RTE.Scratch]; goto $$block49096~j;
  $$block49096~j: assume $IsNotNull(stack3o, Memory); goto $$block49096~i;
  $$block49096~i: assert (this != null); goto $$block49096~h;
  $$block49096~h: stack4i := $Heap[this, RTE.MSP]; goto $$block49096~g;
  $$block49096~g: assume InRange(stack4i, System.Int32); goto $$block49096~f;
  $$block49096~f: stack5i := 4; goto $$block49096~e;
  $$block49096~e: stack4i := (stack4i - stack5i); goto $$block49096~d;
  $$block49096~d: call stack3i := RTE.ReadQuad$Memory$notnull$System.Int32(stack3o, stack4i); goto $$block49096~c;
  $$block49096~c: assume InRange(stack3i, System.Int32); goto $$block49096~b;
  $$block49096~b: stack2i := (stack2i * stack3i); goto $$block49096~a;
  $$block49096~a: call RTE.WriteQuad$Memory$notnull$System.Int32$System.Int32(stack0o, stack1i, stack2i); goto block49130;
  
}

axiom $IsInterface(Microsoft.Contracts.ICheckedException);
axiom (forall K : name :: {(Microsoft.Contracts.ICheckedException <: K)} ((Microsoft.Contracts.ICheckedException <: K) <==> ((Microsoft.Contracts.ICheckedException == K) || (System.Object == K))));
procedure RTE..cctor();
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o : ref, $f : name :: (((((($f != $inv) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (old($Heap)[$o, $writable] == true)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) ==> (old($Heap[$o, $f]) == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) || (old($Heap)[$o, $allocated] != true)));
  free ensures (forall $o : ref :: (old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]));
  

